\begin{tabbing}
@$i$ locl($a$) occurs once
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$\exists$$e$@$i$.kind($e$) $=$ locl($a$)\+
\\[0ex]\& $\forall$$e$@$i$. $\forall$${\it e'}$@$i$. kind($e$) $=$ locl($a$) $\Rightarrow$ kind(${\it e'}$) $=$ locl($a$) $\Rightarrow$ $e$ $=$ ${\it e'}$
\-
\end{tabbing}